COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "206MAC.PUB[206,LSP]" source_file
C00003 00003	.hd206 FALL 1979
C00004 00004	.if false then begin "lam"
C00016 00005	.cb More about $$LAMB$s
C00022 00006	.cb More to do with $LAMB 
C00029 ENDMK
C⊗;
.REQUIRE "206MAC.PUB[206,LSP]" source_file;
.
.odd heading(,,{page}) ;
.even heading({page}, , ) ;
.
.LSPFONT
.basicops 
.
.allops
.itemmac 1;
.
.PORTION MAINPORTION
.hd206 FALL 1979
.PAGE ← 1
.if false then begin "lam"
    .bb Continuing problem.

    #. This problem deals with representation and manipulation of expressions
    in the pure λ-calculus.  The basic properties and
    manipulations of $$LAMB$-expressions are defined and you are asked
    to write the corresponding programs.  The goal is a program that will
    apply a list of reductions to an expression.

	    The simplest λ-expression is a variable, represented
    by a $$LAMB$-variable which is a pair $$(X_._n)$, $$n=0,_1,_2,_...$.
    The class, $$LAMB$-expressions, of S-expressions representing λ-expressions 
    is defined inductively as follows:
    .skip 1
    .begin preface 0 indent 4,8 group

      (i) a $$LAMB$-variable is a $$LAMB$-expression (of sort variable),

     (ii) if ⊗e1 and  ⊗e2 are $$LAMB$-expressions then $$(APPL e1 e1)$
    is a $$LAMB$-expression (of sort application),

    (iii) if ⊗e is a $$LAMB$-expression then for each ⊗n, $$(LAMB_n_e)$ 
    is a $$LAMB$-expression (of sort abstraction), 
    representing abstraction with respect to the ⊗⊗n⊗th variable $$(X_._n)$.

     (iv) These are all of the $$LAMB$-expressions.
    .end

    ##. Write a program ⊗islamb[e] which returns qT if ⊗e is a 
    $$LAMB$-expression and qNIL otherwise.

    [Remark:  you will find programs computing the predicates 
    ⊗var, ⊗appl, and ⊗abstr which are satisfied by the three types of 
    $$LAMB$-expressions useful, here and later.]

	    In the following we will use variable to mean $$LAMB$-variable and
    expression to mean $$LAMB$-expression.  

	    An occurrence of a variable, ⊗v, in an expression ⊗e,  
    can be classified as free or bound as follows.
    If ⊗e is the variable ⊗v, then the occurrence of ⊗v in ⊗e is free in ⊗e.  
    If ⊗e is an abstraction on ⊗v, e.g. ⊗e is of the form $$(LAMB_n_e1)$ and
    ⊗v is $$(X_._n)$ then a free occurrence of ⊗v in ⊗e1 is bound by
    this $$LAMB$.  If ⊗e is of the form $$(LAMB_n_e1)$, where ⊗v is not $$(X_._N)$,
    then an occurrence of ⊗v (in ⊗⊗e1⊗) is bound or free in ⊗e according as it 
    is bound or free in ⊗⊗e1⊗.
    Similarly, if ⊗e is of the form $$(APPL_e1_e2)$, an occurrence of ⊗v in 
    in ⊗⊗e1⊗ (resp. ⊗⊗e2⊗) is bound or free in ⊗e according as it 
    is bound or free in ⊗⊗e1⊗ (resp. ⊗⊗e2⊗).

	    An occurrence of ⊗v in ⊗e is designated by the list of "moves",
    called a ⊗location, necessary to get from ⊗e to the subexpression of ⊗e 
    which is the occurrence of ⊗v.    
    If ⊗e is ⊗v then the location is the empty list.
    If ⊗e is $$(APPL e1 e2)$ and the occurrence is in $e1 then the 
    location is $A1 followed by the list of moves locating $v in $e1. 
    (similarly if the occurrence is in $e2, with $A2 instead of $$A1$.)
    If ⊗e is $$(LAMB m e1)$ then the
    location is $B followed by the list of moves locating $v in $e1.  

    ##.  Write a program ⊗freeoccs[n,e] that returns a list of locations
    of free occurrences of the ⊗⊗n⊗th variable, $$(X_._n)$, in the expression ⊗e.  
    (You may assume ⊗e to be a $$LAMB$-expression.)__
    Thus 

    ⊗⊗⊗freeoccs[$$1$,$$(APPL (LAMB 2 (APPL (X.2) (X.2))) (APPL (X.1) (X.1)))$]=
    $$((A2 A1)(A2 A2))$⊗

    ##. Write a program ⊗substfree[e1,n,e] which substitutes ⊗e1 for
    free occurrences of $$(X_._n)$ in ⊗e.  

	    Note that we haven't provided a means to prevent trapping of free variables
    of ⊗e1.  If $$(X_._m)$ occurrs free in ⊗e1 and ⊗v occurs free in a subexpression
    of ⊗e of the form $$(LAMB_m_e2)$ the occurrence of $$(X_._m)$ in ⊗e1 will
    be "trapped" upon substitution.  That is it will be bound in the resulting
    expression.  This causes undesired behaviour in the λ-calculus, so we
    wish to prevent such substitutions from occuring.

    ##. Write a program ⊗freefor[e1,n,e] which returns qT if no free variable
    of ⊗e1 will become bound upon substitution of ⊗e1 for each free occurrence
    of $$(X_._n)$ in ⊗e.   

	    Since we don't want to be stuck just because some expression is not
    "freefor" we provide a means of modifying the expression ⊗e 
    so that ⊗e1 will be free for ⊗v in ⊗e.   
    This is known as renaming of bound variables.
    It is accomplished for a variable $$(X_._n)$, by choosing a variable $$(X_._m)$ 
    that is unused so far and replacing each subexpression of ⊗e of the form
    $$(LAMB_n_e2)$ by $$(LAMB_m_e3)$ ⊗e3 is obtained from ⊗e2 by replacing
    each occurrence of $$(X_._n)$ in ⊗e2 bound by this $LAMB by $$(X_._m)$.

    ##. Write a program ⊗rename[n,m,e] that renames $$(X_._n)$ to $$(X_._m)$
    in ⊗e as outlined above.   

	    Now we have all of the basic programs needed to manipulate 
    $$LAMB$-expressions, carry out reductions, look for normal forms, etc.
    For example we can apply a list of reductions to an expression.  There
    are two basic reductions.  First, $$(ALPHA_n_m)$ applied to ⊗e is 
    ⊗⊗rename[n,m,e]⊗.  It applies only if $$(X_._m)$ does not occur in ⊗e.  
    Second, $BETA applies only to expressions ⊗e of the form $$(APPL_e1_e2)$
    where ⊗e1 is an abstraction $$(LAMB_n_e3)$ and ⊗e2 is free for $$(X_._n)$
    in ⊗e1.  The result of applying $BETA to ⊗e is ⊗⊗substfree[e2,n,e1]⊗.
    We generalize these reductions to apply to subxexpressions of an
    expression ⊗e.  Thus $$(ALPHA_n_m_loc)$ applied to ⊗e is obtained by
    replacing the subexpression located at ⊗loc by the result of applying
    $$(ALPHA_n_m)$ to that subexpression.  It only applies if ⊗loc is
    a valid location in ⊗e and the $ALPHA reduction applies to that subexpression.
    Similarly for $$(BETA_loc)$.

    ##.  Write a program ⊗⊗LAMB-reduce[e,rlist]⊗ that applies a list of
    reductions to a $$LAMB$-expression.  
    The program should be robust in the following sense.  It should check that
    ⊗e is a $$LAMB$-expression and return an appropriate message if not.  It
    should check each element of ⊗rlist to see that it denotes a reduction and
    complain if not.  Before a reduction is applied, a check should be made
    that is does indeed apply and appropriate complaints made if not.

    .begin nofill group
    Some examples follow.  Let

	    ⊗⊗e=$$(LAMB_0_(APPL_(X_._1)_(X_._0)))$⊗
	    ⊗⊗e1=$$(LAMB_1_(APPL_(X_._0)_(X_._1)))$⊗
	    ⊗⊗e2=$$(LAMB_2_(APPL_(X_._2)_(X_._1)))$⊗
	    ⊗⊗e3=$$(LAMB_2_(APPL_(X_._2)_(LAMB_1_(APPL_(X_._0)_(X_._1)))))$⊗
	    ⊗⊗e4=$$(APPL (LAMB_1_(LAMB_0_(APPL_(X_._1)_(X_._0))))$⊗
	    __________$$(LAMB_1_(APPL_(X_._0)_(X_._1))))$
	    ⊗⊗rlist=$$((ALPHA_0_2_NIL) (BETA NIL))$⊗

    then

	    ⊗⊗freefor[e1,$$1$,e]=qNIL⊗
	    ⊗⊗rename[$$0$,$$2$,e]=e2⊗
	    ⊗⊗freefor[e1,$$1$,e2]=qT⊗
	    ⊗⊗substfree[e1,$$1$,e2]=e3⊗
	    ⊗⊗LAMB-reduce[e4,rlist]=e3]⊗
    .end

	    After we discuss sequential programs and I/O, we will see
    how ⊗LAMB-reduce can be converted in to an interactive program that
    you can have various conversations with about $$LAMB$-expressions.

    .END


.end "lam"
.cb More about $$LAMB$s

	This is a continuation of problem 5 in Homework 1.   
First a bit of background.   
The Lambda-calculus was devised by Alonzo Church in the
1930's to study the concept of computable function.   
He developed the λ-notation, set down conversion rules such as 
$ALPHA and $BETA, and studied the properties of the resulting
system.  He also show how to represent numbers and functions on
numbers in this system.  His monograph
"The Calculi of Lambda-Conversion", Annals of Math. Studies No. 6,
(1941) is an excellent survey of this work.   

For your amusement here are some of the things that can be represented
as $$LAMB$-expressions.  The thing being represented is on the 
lefthand side of the "→" and the representation is on the right.

#. Positive numbers.
.begin nofill indent 4,4

1 → $$(LAMB 1(LAMB 0(APPL(X.1)(X.0))))$
2 → $$(LAMB 1(LAMB 0(APPL(X.1)(APPL(X.1)(X.0)))))$
3 → $$(LAMB 1(LAMB 0(APPL(X.1)(APPL(X.1)(APPL(X.1)(X.0))))))$
etc.

⊗add1 → $$(LAMB 2(LAMB 1(LAMB 0(APPL(X.1)(APPL(APPL(X.2)(X.1))(X.0))))))$
⊗plus  → $$(LAMB 3(LAMB 2(LAMB 1(LAMB 0$
         $$_______(APPL(APPL(X.3)(X.1))(APPL(APPL(X.2)(X.1))(X.0)))))))$
⊗times → $$(LAMB 3(LAMB 2(LAMB 1(APPL(X.3)(APPL(X.2)(X.1))))))$
⊗exp → $$(LAMB 3(LAMB 2(APPL(X.3)(X.2))))$
.end

#. Pairing and selecting the first and second components of a pair.
.begin nofill indent 4,4

⊗pair → $$(LAMB 3(LAMB 2(LAMB 1(APPL(APPL(X.1)(X.3))(X.2)))))$
⊗p1 → $$(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(APPL(APPL(X.3)(LAMB 0(X.0)))(X.2))))))$
⊗p2 → $$(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(APPL(APPL(X.2)(LAMB 0(X.0)))(X.3))))))$
.end

#. Tripling and selecting the first, second, and third components of a triple.
.begin nofill indent 4,4

⊗trip → $$(LAMB 4(LAMB 3(LAMB 2(LAMB 1 $
        $$________(APPL(APPL(APPL(X.1)(X.4))(X.3))(X.2))))))$
⊗t1 → $$(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(LAMB 4$
      $$________(APPL(APPL(APPL(APPL(X.3)$
      $$________________(LAMB 0(X.0)))(X.4))(LAMB 0(X.0)))(X.2)))))))$
⊗t2 → $$(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(LAMB 4$
      $$________(APPL(APPL(APPL(APPL(X.2)$
      $$________________(LAMB 0(X.0)))(X.4))(LAMB 0(X.0)))(X.3)))))))$
⊗t3 → $$(LAMB 1(APPL(X.1)(LAMB 2(LAMB 3(LAMB 4$
      $$________(APPL(APPL(APPL(APPL(X.2)$
      $$________________(LAMB 0(X.0)))(X.3))(LAMB 0(X.0)))(X.4)))))))$
.end

The sense in which the $$LAMB$-expressions represent things, is that
after doing appropriate reductions (and renaming of bound variables)
the result of "applying" the representation of a function to the repsentation
of its argument(s) is a representation of the result of applying the function 
to the argument(s) in the ordinary sense.   
For example ⊗⊗add1[1]⊗ is represented by the expression 
$$(APPL λ[add1] λ[1])$, where $λ[thing] is shorthand for the $$LAMB$-representation
of $thing as given above.  As a $$LAMB$-expression it be reduces to the 
expression representing 2.  Given any two expressions $e1, $e2, 
$$(APPL(APPL λ[pair] e1) e2)$ represents the ⊗pair[e1,e2] and 
$$(APPL λ[p1] (APPL(APPL λ[pair] e1) e2))$ represents ⊗p1[pair[e1,e2]] and 
as a $$LAMB$-expression reduces to $e1 as it should.
Thus arithmetic is represented accurately (on representations of numbers)
and the representations ⊗pair,p1,p2 obey rules similar to those for
qqa, qqd, and qcons acting on S-expressions.
The representations of ⊗trip,t1,t2,t3 behave analogously.

You should use these ideas to exercise your interpreter and try out
some non-trivial reductions which have some meaning.

.cb More to do with $LAMB 
.item ← 0

#.  Using the basic routines for manipulating $LAMBs you can
write an interactive interpreter that will accept a variety of
commands and take appropriate actions.  Here are some ideas.

##.  A $DEFINE command to give names to particular $$LAMB$-expressions.
You should then extend the ability to recognize expressions to include
defined names where ever an expression could occur.  Thus if $ONE and
$add1 were defined as above $$(APPL add1 ONE)$ would be a valid expression
and should be expanded by your interpreter using the definition before
attempting to any computation with the expression.  

##.  An $ALPHA command that takes an expression and two numbers 
(and possibly a subexpression designation) and does an $ALPHA conversion.

##.  A $BETA command that takes an expression 
(and possibly a subexpression designation) and does an $BETA conversion
if allowed.

##.  A $BETA! command that takes an expression 
(and possibly a subexpression designation) and does an $BETA conversion
first doing any necessary remaning of bound variables.  Thus it will
have to discover what variables are to be renamed and figure out 
a safe name (for example $(X.n) for the least $n such that $(X.n) doesn't 
occur in the given expression).

##. Commands for building sequences of reductions.   One way is to have 
a notion of current reduction (undefined initially).  Each sequence
should have a name so you can switch to that as the current reduction.
You will need a command to start a new reduction which should take a name
and an expression, to be the first member of the sequence.
The above reduction commands can apply to the some element
of the reduction sequence to extend it.  The command for switching attention
to a new current reduction sequence should save the old one in such a manner
that it can be retrieved by name later.  (Association lists and property lists
are good for such things.)  You will also need a command to print any
given reduction sequence.

##.  Any other commands that seem like fun to implement.

.if lines≤10 then next page;

#.  As a basis for your LAMB interpreter you should have programs
⊗islamb, ⊗mklamb, ⊗bvarof, ⊗body, ⊗isappl, ⊗mkappl, ⊗funof, ⊗argof and
⊗isvar to test for, construct and take apart the various types
of $$LAMB$-expressions.  Such auxiliary programs make the main
programs more readable, but require extra function calls when
these programs are executed.  You should replace these auxiliary
program definitions by suitable $MACRO definitions.  This helps
make readability and efficiency more compatible.

#.  Modify the error checking parts of your program to use the MACLISP
primitives $CATCH and $THROW.  Cleverly done this can get the
appropriate message to the appropriate place without explicitly
carrying around an extra parameter, or checking every time
a called routine returns to see if it succeeded.

#.  You may have noticed that the notation for $$LAMB$-expressions
is not as compact or flexible as it might be.  Devise some
``shorthand'' that your interpreter can understand.  It should
read the short forms, convert to standard form for manipulation,
and print the results in some standard shorthand.
Some possible abbreviations are:
.begin nofill select 6 indent 8,8

(LAMB n (LAMB m body)) ↔ (LAMB (n m) body)
(APPL (APPL e1 e2) e3) ↔ (APPL e1 e2 e3)
.end
You may wish to think up fancier ones.

#.  If you are adventurous, think about using the destructive operations
$RPLACA and $RPLACD to carry out some of the substitutions made on
$$LAMB$-expressions.   First consider when such action is safe and
reasonable.  Note that if the structure you are modifying is part of
more the one expression, you can get very strange results if you are not
careful.  Sometimes initially copying an expression that you wish to
modify many times and then doing modifications destructively is
successful and reasonable.